Skip to content

Conversation

@atomb
Copy link
Contributor

@atomb atomb commented Sep 22, 2025

Now we can eliminate loops from any statement type that implements a few key operations (not, havoc, assert, assume).

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

Now we can eliminate loops from any statement type that implements a few
key operations (not, havoc, assert, assume).
@aqjune-aws
Copy link
Contributor

It seems conflicts with the main branch must be resolved - do you want to fix it?

Copy link
Contributor

@aqjune-aws aqjune-aws left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It seems there are still uses of HasBoolNeg in DL/Imperative/SemanticsProps.lean . I think they weren't caught during lake build because it was not included in DL/Imperative/Imperative.lean - should we include it?

And make sure the file they're in gets included in the build.
@atomb
Copy link
Contributor Author

atomb commented Oct 31, 2025

It seems there are still uses of HasBoolNeg in DL/Imperative/SemanticsProps.lean . I think they weren't caught during lake build because it was not included in DL/Imperative/Imperative.lean - should we include it?

Good catch! Should be fixed now.

@atomb atomb enabled auto-merge October 31, 2025 21:39
Copy link
Contributor

@MikaelMayer MikaelMayer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

NIce generalization

@atomb atomb added this pull request to the merge queue Nov 6, 2025
Merged via the queue into main with commit c23e469 Nov 6, 2025
10 checks passed
@atomb atomb deleted the generalize-loop-elim branch November 6, 2025 16:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

5 participants